D:Dsys, L:Id List.
(i:Id. (i  L)  ma-is-empty(M(i)))
 (i:Id. Feasible(M(i)))
 (iL.
 (ltgma-outlinks(M(i);i).
 ((destination(1of(ltg))  L)  interface-check(D;1of(ltg);1of(2of(ltg));2of(2of(ltg))))
 Feasible(D) 

latex

Definitions

x:A. B(x), P  Q, P  Q, Feasible(D), P & Q, t  T, Prop, x. t(x), M.dout(l,tg), f(x)?z, if b t else f fi, true, false, 1of(t), 2of(t), ma-outlinks(M;i), da-outlinks(da;i), x:A. B(x), A & B, (x  l), rcv(l,tg), has-src(i;k), p  q, isrcv(k), lnk(k), isl(x), outl(x), da-outlink-f(da;k), tag(k), M.din(l,tg), , mk-ma, , Top, x  dom(f), deq-member(eq;x;L), reduce(f;k;as), Y, P  Q, P  Q, x(s), Dec(P), , Unit, MsgA, Valtype(da;k), xL. P(x), , interface-check(D;l;tg;T), A, False, a:A fp B(a), M sends on link l, b, map(f;as), , fpf-dom-list(f)

Lemmas

l all wf, Id wf, IdLnk wf, ma-outlinks wf, d-m wf, l member wf, ldst wf, pi1 wf, interface-check wf, pi2 wf, ma-feasible wf, assert wf, ma-is-empty wf, dsys wf, decidable assert, deq-member wf, id-deq wf, lsrc wf, assert-deq-member, not functionality wrt iff, fpf-dom wf, Knd wf, Kind-deq wf, rcv wf, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, msga wf, fpf-trivial-subtype-top, fpf-ap wf, member map filter, has-src wf, da-outlink-f wf, assert-has-src, isrcv wf, fpf-dom-list wf, subtype rel list, length wf1, select wf, assert-eq-id, ma-din wf, ma-dout wf, assert-ma-is-empty, top wf, finite-decidable-set, ma-sends-on wf, decidable cand, decidable equal Id, map wf, concat wf, member-concat, exists functionality wrt iff, and functionality wrt iff, member map, idlnk-deq wf